Step of Proof: adjacent-before 11,40

Inference at * 1 1 
Iof proof for Lemma adjacent-before:



1. T : Type
2. L : T List
3. x : T
4. y : T
5. i : {0..(||L|| - 1)}
6. x = L[i]
7. y = L[(i+1)]
8. i@0 : {0..1}
  if (i@0 = 0) then i else i+1 fi  < if (i@0+1 = 0) then i else i+1 fi  
latex

 by InteriorProof (if (((first_nat 2:n)) = 0) then (Repeat (((SplitOnConclITE) 
CollapseTHEN (
CollapseTHEN (Auto')))) else (RepeatFor (first_nat 2:n) (((SplitOnConclITE) 
CollapseTHEN (
CollapseTHEN (Auto'))))) 
latex


C.


Definitions{x:AB(x)} , ||as||, i  j , if b then t else f fi , left + right, Unit, i j, i <z j, p q, p  q, p  q, [d], a < b, x f y, f(a), a < b, null(as), x =a y, P  Q, P & Q, x:A  B(x), P  Q, tt, b, , ff, , , (i = j), n+m, #$n, l[i], b, x:AB(x), x:AB(x), t  T, A, s = t, {i..j}, type List, Type, a < b
Lemmasifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf

origin